Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    p1 + p1  → p2
2:    p1 + (p2 + p2)  → p5
3:    p5 + p5  → p10
4:    (x + y) + z  → x + (y + z)
5:    p1 + (p1 + x)  → p2 + x
6:    p1 + (p2 + (p2 + x))  → p5 + x
7:    p2 + p1  → p1 + p2
8:    p2 + (p1 + x)  → p1 + (p2 + x)
9:    p2 + (p2 + p2)  → p1 + p5
10:    p2 + (p2 + (p2 + x))  → p1 + (p5 + x)
11:    p5 + p1  → p1 + p5
12:    p5 + (p1 + x)  → p1 + (p5 + x)
13:    p5 + p2  → p2 + p5
14:    p5 + (p2 + x)  → p2 + (p5 + x)
15:    p5 + (p5 + x)  → p10 + x
16:    p10 + p1  → p1 + p10
17:    p10 + (p1 + x)  → p1 + (p10 + x)
18:    p10 + p2  → p2 + p10
19:    p10 + (p2 + x)  → p2 + (p10 + x)
20:    p10 + p5  → p5 + p10
21:    p10 + (p5 + x)  → p5 + (p10 + x)
There are 26 dependency pairs:
22:    (x + y) +# z  → x +# (y + z)
23:    (x + y) +# z  → y +# z
24:    p1 +# (p1 + x)  → p2 +# x
25:    p1 +# (p2 + (p2 + x))  → p5 +# x
26:    p2 +# p1  → p1 +# p2
27:    p2 +# (p1 + x)  → p1 +# (p2 + x)
28:    p2 +# (p1 + x)  → p2 +# x
29:    p2 +# (p2 + p2)  → p1 +# p5
30:    p2 +# (p2 + (p2 + x))  → p1 +# (p5 + x)
31:    p2 +# (p2 + (p2 + x))  → p5 +# x
32:    p5 +# p1  → p1 +# p5
33:    p5 +# (p1 + x)  → p1 +# (p5 + x)
34:    p5 +# (p1 + x)  → p5 +# x
35:    p5 +# p2  → p2 +# p5
36:    p5 +# (p2 + x)  → p2 +# (p5 + x)
37:    p5 +# (p2 + x)  → p5 +# x
38:    p5 +# (p5 + x)  → p10 +# x
39:    p10 +# p1  → p1 +# p10
40:    p10 +# (p1 + x)  → p1 +# (p10 + x)
41:    p10 +# (p1 + x)  → p10 +# x
42:    p10 +# p2  → p2 +# p10
43:    p10 +# (p2 + x)  → p2 +# (p10 + x)
44:    p10 +# (p2 + x)  → p10 +# x
45:    p10 +# p5  → p5 +# p10
46:    p10 +# (p5 + x)  → p5 +# (p10 + x)
47:    p10 +# (p5 + x)  → p10 +# x
The approximated dependency graph contains one SCC: {24,25,27,28,30,31,33,34,36-38,40,41,43,44,46,47}.
Tyrolean Termination Tool  (48.78 seconds)   ---  May 4, 2006